(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const v9 Bool)
(declare-const v10 Bool)
(declare-const i2 Int)
(declare-const i3 Int)
(declare-const i4 Int)
(declare-const i10 Int)
(declare-const i11 Int)
(declare-const i12 Int)
(declare-const i13 Int)
(declare-const i14 Int)
(assert (exists ((q0 Bool) (q1 Bool)) (not (distinct q1 v4 q1 v0 v6 q1 q1))))
(assert (not (exists ((q2 Int) (q3 Bool)) (=> (<= q2 q2) (=> v4 q3)))))
(assert (not (exists ((q4 Bool)) (not (not v8)))))
(assert (exists ((q5 Bool) (q6 Int)) (not (distinct v3 v8 q5 (= v9 (< i14 i14) v5 v9 v7) v4 (= v9 (< i14 i14) v5 v9 v7) (< i14 i14) v2))))
(declare-const v11 Bool)
(declare-const i15 Int)
(declare-const v12 Bool)
(declare-const v13 Bool)
(assert (not (exists ((q7 Int) (q8 Bool) (q9 Bool) (q10 Int)) (=> (> q7 i2) (not v7)))))
(assert (exists ((q11 Int) (q12 Int)) v2))
(declare-const v14 Bool)
(declare-const v15 Bool)
(assert (or (distinct 91 179) (and (< i14 i14) (= v9 (< i14 i14) v5 v9 v7) v12 (<= (mod 62 56) i2) v4 v0 v13) (and (< i14 i14) (= v9 (< i14 i14) v5 v9 v7) v12 (<= (mod 62 56) i2) v4 v0 v13)))
(assert (or v2 (and (< i14 i14) (= v9 (< i14 i14) v5 v9 v7) v12 (<= (mod 62 56) i2) v4 v0 v13) v10))
(assert (or (not (<= (mod 62 56) i2)) (and (< i14 i14) (= v9 (< i14 i14) v5 v9 v7) v12 (<= (mod 62 56) i2) v4 v0 v13) (= (mod 62 56) 57)))
(assert (or v10 v2 (not (<= (mod 62 56) i2))))
(check-sat)
